\begin{tabbing}
ESAxioms\=\{i:l\}\+
\\[0ex]($E$; $T$; $M$; ${\it loc}$; ${\it kind}$; ${\it val}$; ${\it when}$; ${\it after}$; ${\it sends}$; ${\it sender}$; ${\it index}$; ${\it first}$; ${\it pred}$; ${\it causl}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:$E$, ${\it e'}$:$E$. ${\it loc}$($e$) $=$ ${\it loc}$(${\it e'}$) $\in$ Id $\Rightarrow$ ${\it causl}$($e$,${\it e'}$) $\vee$ $e$ $=$ ${\it e'}$ $\in$ $E$ $\vee$ ${\it causl}$(${\it e'}$,$e$))\+
\\[0ex]\& ($\forall$$e$:$E$. ${\it first}$($e$) $\Leftrightarrow$ ($\forall$${\it e'}$:$E$. ${\it loc}$(${\it e'}$) $=$ ${\it loc}$($e$) $\in$ Id $\Rightarrow$ $\neg$${\it causl}$(${\it e'}$,$e$)))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]$\neg$${\it first}$($e$)
\\[0ex]$\Rightarrow$ \=${\it loc}$(${\it pred}$($e$)) $=$ ${\it loc}$($e$) $\in$ Id \& ${\it causl}$(${\it pred}$($e$),$e$)\+
\\[0ex]\& ($\forall$${\it e'}$:$E$. ${\it loc}$(${\it e'}$) $=$ ${\it loc}$($e$) $\in$ Id $\Rightarrow$ $\neg$(${\it causl}$(${\it pred}$($e$),${\it e'}$) \& ${\it causl}$(${\it e'}$,$e$))))
\-\-\\[0ex]\& ($\forall$$e$:$E$. $\neg$${\it first}$($e$) $\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) $=$ ${\it after}$($x$,${\it pred}$($e$)) $\in$ $T$(${\it loc}$($e$),$x$)))
\\[0ex]\& (Trans $e$,${\it e'}$:$E$. ${\it causl}$($e$,${\it e'}$))
\\[0ex]\& strongwellfounded($E$; $e$,${\it e'}$.(${\it causl}$($e$,${\it e'}$)))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]isrcv(${\it kind}$($e$))
\\[0ex]$\Rightarrow$ \=(${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$)))[${\it index}$($e$)]\+
\\[0ex]$=$
\\[0ex]msg(lnk(${\it kind}$($e$));tag(${\it kind}$($e$));${\it val}$($e$))
\\[0ex]$\in$ Msg($M$))
\-\-\\[0ex]\& ($\forall$$e$:$E$. isrcv(${\it kind}$($e$)) $\Rightarrow$ ${\it causl}$(${\it sender}$($e$),$e$))
\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]${\it causl}$($e$,${\it e'}$)
\\[0ex]$\Rightarrow$ \=$\neg$${\it first}$(${\it e'}$) \& ${\it causl}$($e$,${\it pred}$(${\it e'}$)) $\vee$ $e$ $=$ ${\it pred}$(${\it e'}$) $\in$ $E$\+
\\[0ex]$\vee$ isrcv(${\it kind}$(${\it e'}$)) \& ${\it causl}$($e$,${\it sender}$(${\it e'}$)) $\vee$ $e$ $=$ ${\it sender}$(${\it e'}$) $\in$ $E$)
\-\-\\[0ex]\& ($\forall$$e$:$E$. isrcv(${\it kind}$($e$)) $\Rightarrow$ ${\it loc}$($e$) $=$ destination(lnk(${\it kind}$($e$))) $\in$ Id)
\\[0ex]\& ($\forall$$e$:$E$, $l$:IdLnk. $\neg$${\it loc}$($e$) $=$ source($l$) $\in$ Id $\Rightarrow$ ${\it sends}$($l$,$e$) $=$ nil $\in$ Msg\_sub($l$;$M$) List)
\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]isrcv(${\it kind}$($e$))
\\[0ex]$\Rightarrow$ isrcv(${\it kind}$(${\it e'}$))
\\[0ex]$\Rightarrow$ lnk(${\it kind}$($e$)) $=$ lnk(${\it kind}$(${\it e'}$)) $\in$ IdLnk
\\[0ex]$\Rightarrow$ (\=${\it causl}$($e$,${\it e'}$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex]${\it causl}$(${\it sender}$($e$),${\it sender}$(${\it e'}$))
\\[0ex]$\vee$ ${\it sender}$($e$) $=$ ${\it sender}$(${\it e'}$) $\in$ $E$ \& ${\it index}$($e$)$<$${\it index}$(${\it e'}$)))
\-\-\\[0ex]\& (\=$\forall$$e$:$E$, $l$:IdLnk, $n$:\{0..$\parallel$${\it sends}$($l$,$e$)$\parallel^{-}$\}.\+
\\[0ex]$\exists$${\it e'}$:$E$.
\\[0ex]isrcv(${\it kind}$(${\it e'}$))
\\[0ex]\& lnk(${\it kind}$(${\it e'}$)) $=$ $l$ $\in$ IdLnk \& ${\it sender}$(${\it e'}$) $=$ $e$ $\in$ $E$ \& ${\it index}$(${\it e'}$) $=$ $n$ $\in$ $\mathbb{Z}$)
\-\-
\end{tabbing}